ee'.P(e) == e:es-E(es). (es-le(es; e; e') c P(e)) 

latex

---

clarification:

existse-le(es;e';e.P(e)) == e:es-E(es). (es-le(es; e; e') c P(e)) 

latex

Definitions	x:A. B(x), es-E(es), A c B, es-le(es; e; e')
FDL editor aliases	existse-le